The subject matter disclosed herein relates to software verification and, more specifically, to the automated generation of test cases and/or test procedures used during software verification.
Software verification is an important phase in the software development life cycle. Software verification generally involves the application of test cases, which may be in the form of a textual description of the test objectives, and test procedures, which typically contain test steps and test data and may be in the form of executable test scripts, depending on the software programming language and the specific testing platform. In certain fields, such as aviation control systems, extensive formal verification of control software may be required before the software can be deployed for use. Test case and/or test procedure generation, in particular, is an important aspect of software testing that is often a labor-intensive and time-consuming task. For example, more than 50% of total software development costs are often spent generating test case data and test steps manually from software requirements. As such, automated test case and test procedure generation can be beneficial to the software verification process.
Test case data is typically generated based on various software artifacts. For example, test case data may be generated using the software program structure and/or source code, information about the input/output data space, and/or information dynamically obtained from program execution. In particular, for model-based testing, test case data can be generated using the software specification and/or design models.
Model-based software verification generally uses software models to describe the possible input/output sequences on a chosen level of abstraction, and is linked to the low-level design implementation by a conformance relation. A test generation algorithm may be used to derive test case data from the software model by selecting a finite subset from the potentially infinite set of sequences specified by the model, and testing criterion may be applied to justify the adequateness of the selection. The test generation algorithm could use a combination of constraint solving, theorem proofing, and symbolic execution technologies to enable automatic test generation. The testing criterion can be based on numerous criteria, including requirements coverage and structure coverage like model coverage.
Automatic test case generation is possible for certain types of software. For example, test case data can be generated for software that includes only Boolean logic expressions, linear operations, and/or polynomial functions, since these expressions and functions can be easily solved through mathematical programming, constraint solving, and model checking. However, other software may include one or more nonlinear arithmetic functions that extend over Real number ranges (e.g., trigonometric functions, logarithm functions, exponential functions), and these functions are intrinsically hard and remain unsolved. As such, there remains a need for automatic test case generation for software that includes nonlinear arithmetic functions over Real number ranges.